\begin{tabbing}
d{-}comp($D$;$v$;${\it sched}$;${\it dec}$)($t$,$f$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=let $s$ = $\lambda$$i$.if $t$=$_{2}$0$\rightarrow$ $\lambda$$x$.d{-}m($D$; $i$).init($x$)?$v$($i$,$x$) else 1of($f$($t$$-$1,$i$)) fi in \+
\\[0ex]$\lambda$$i$.\=let ${\it si}$ = $s$($i$) in \+
\\[0ex]let $w$ = d{-}partial{-}world($D$;$f$;$t$;$s$) in 
\\[0ex]let $a$ = \=Case ${\it sched}$($i$) of\+
\\[0ex]inl($f$) $\Rightarrow$ \=Case $f$($t$) of\+
\\[0ex]inl($l$) $\Rightarrow$ \=if \=destination($l$) = $i$ $\wedge_{2}$ 0$<_{2}\parallel$w{-}queue($w$; $l$; $t$)$\parallel\rightarrow$\+\+
\\[0ex]doact\=(rcv($l$,mtag(hd(w{-}queue($w$; $l$; $t$))))\+
\\[0ex];mval(hd(w{-}queue($w$; $l$; $t$))))
\-\-\\[0ex]else null fi
\-\\[0ex]inr($a$) $\Rightarrow$ \=if isl(${\it dec}$($i$,$a$,${\it si}$))$\rightarrow$ doact(inr($a$);outl(${\it dec}$($i$,$a$,${\it si}$)))\+
\\[0ex]else null fi
\-\-\\[0ex]inr($x$) $\Rightarrow$ null in 
\-\\[0ex]let $m$ = \=if isl($a$)$\rightarrow$ nil\+
\\[0ex]else filter\=($\lambda$$m$.source(mlnk($m$)) = $i$\+
\\[0ex];d{-}m($D$; $i$).sends(1of(outr($a$)),${\it si}$,2of(outr($a$)))) fi in 
\-\-\\[0ex]let ${\it s'}$ = \=if isl($a$)$\rightarrow$ ${\it si}$\+
\\[0ex]else $\lambda$$x$.d{-}m($D$; $i$).ef(1of(outr($a$)),$x$,${\it si}$,2of(outr($a$)))?${\it si}$($x$) fi in 
\-\\[0ex]$\langle$${\it s'}$$,\,$$a$$,\,$$m$$\rangle$
\-\-
\end{tabbing}